A, B:Type, f:(AB), ds:(IdType), da:(IdKndType).
trivial-component(f) |- es,in,out.g:E(out)E(in)
trivial-component(f) |- es,in,out.((e:E(out). g(e) c e & out(e) = f(in(g(e)))  B)
trivial-component(f) |- es,in,out.& (e, e':E(out). (e < e')  (g(e) < g(e')))) 

latex

Definitions

ff, if b then t else f fi , tt, {T}, SQType(T), p  q, Top, b, False, A, A  B, , P  Q, True, T, P  Q, A c B, t  T, x. t(x), , scheme-constant(R), let x,y,z = a in t(x;y;z), scheme-none(), es-decl(es;ds;da), P  Q, S |-es.P(es), P  Q, e c e', P & Q, E(X), x:A. B(x), trivial-component(f), C |- es,in,out.P(es;in;out), x:A. B(x), outl(x), do-apply(f;x), Unit, , SqStable(P), x(s),

Lemmas

interface-compose-val, false wf, assert of bnot, eqff to assert, not wf, bnot wf, iff transitivity, can-apply wf, eqtt to assert, bool wf, bool sq, is-interface-compose, es-le weakening eq, es-le-causle, abs-interface-compose, interface wf, Id wf, le wf, Namer wf, rev implies wf, decidable assert, sq stable from decidable, es-interface-val wf, es-causl wf, top wf, interface-compose wf, abs-interface wf, es-is-interface wf, es-kindtype wf, hasloc wf, assert wf, Knd wf, es-state wf, R-none-rule